---------------------------- MODULE CapabilitySystem ---------------------------

EXTENDS Naturals, Sequences, FiniteSets

(*
 * ZENrs 能力系统形式化模型
 * 
 * 本模型描述了ZENrs exokernel中能力系统的关键属性和行为，
 * 用于验证能力隔离、权限传递、所有权管理等安全机制的正确性。
 *)

(* 类型定义 *)
CapabilityId == Int
OwnerId == Int

(* 能力类型 *)
CapabilityType == {"memory", "cpu", "io", "interrupt"}

(* 能力权限 *)
CapabilityPermission == {"read", "write", "execute"}

(* 资源类型 *)
ResourceType == CapabilityType

(* 内存资源数据 *)
MemoryResourceData == [
    base : Int,
    size : Int
]

(* CPU资源数据 *)
CpuResourceData == [
    priority : Int
]

(* IO资源数据 *)
IoResourceData == [
    port_start : Int,
    port_end : Int
]

(* 中断资源数据 *)
InterruptResourceData == [
    irq_start : Int,
    irq_end : Int
]

(* 资源数据联合类型 *)
ResourceData == [
    type : CapabilityType,
    data : CHOOSE d : 
        (type = "memory" => d \in MemoryResourceData) /\
        (type = "cpu" => d \in CpuResourceData) /\
        (type = "io" => d \in IoResourceData) /\
        (type = "interrupt" => d \in InterruptResourceData)
]

(* 能力结构 *)
Capability == [
    id : CapabilityId,
    type : CapabilityType,
    owner_id : OwnerId,
    permissions : [
        read : Bool,
        write : Bool,
        execute : Bool
    ],
    resource_data : ResourceData
]

(* 能力管理器状态 *)
CapabilityManagerState == [
    capabilities : Seq(Capability),
    next_cap_id : CapabilityId,
    service_layer_mem_cap : CapabilityId,
    service_layer_cpu_cap : CapabilityId
]

(* 初始状态 *)
Init == 
    [
        capabilities |-> << >>,
        next_cap_id |-> 1,
        service_layer_mem_cap |-> 0,
        service_layer_cpu_cap |-> 0
    ]

(* 创建新能力 *)
CreateCapability(cms, resource_data) == 
    LET
        cap_id == cms.next_cap_id
        new_cap == [
            id |-> cap_id,
            type |-> resource_data.type,
            owner_id |-> 0,  (* 初始拥有者为内核 *)
            permissions |-> [read |-> TRUE, write |-> TRUE, execute |-> TRUE],  (* 初始权限 *)
            resource_data |-> resource_data
        ]
        
        new_capabilities == Append(cms.capabilities, new_cap)
    IN
        [cms EXCEPT 
            !capabilities = new_capabilities,
            !next_cap_id = cms.next_cap_id + 1
        ]

(* 获取能力 *)
AcquireCapability(cms, cap_id) == 
    LET
        (* 在实际系统中，这里会增加引用计数 *)
        (* 这里简化处理，只是验证能力存在 *)
        cap_exists == \E c \in cms.capabilities : c.id = cap_id
    IN
        IF cap_exists THEN 
            cms  (* 返回原状态，实际系统中会更新引用计数 *)
        ELSE 
            cms  (* 返回原状态，获取失败 *)

(* 释放能力 *)
ReleaseCapability(cms, cap_id) == 
    LET
        (* 在实际系统中，这里会减少引用计数 *)
        (* 当引用计数为零时，可能会回收资源 *)
        (* 这里简化处理，只是记录操作 *)
    IN
        cms  (* 返回原状态，实际系统中会更新引用计数 *)

(* 检查能力权限 *)
CheckCapabilityPermission(cms, cap_id, resource_type, permission) == 
    LET
        found_cap == CHOOSE c \in cms.capabilities : c.id = cap_id
        
        has_permission == IF found_cap # "" THEN 
            (found_cap.type = resource_type) /\ 
            (permission = "read" => found_cap.permissions.read) /\
            (permission = "write" => found_cap.permissions.write) /\
            (permission = "execute" => found_cap.permissions.execute)
        ELSE 
            FALSE
    IN
        has_permission

(* 派生新能力 *)
DeriveCapability(cms, parent_cap_id, new_permissions, resource_subset) == 
    LET
        parent_cap == CHOOSE c \in cms.capabilities : c.id = parent_cap_id
        
        (* 检查父能力是否存在且有效 *)
        parent_valid == parent_cap # ""
        
        (* 检查请求的权限是否不超过父能力的权限 *)
        permissions_valid == 
            (new_permissions.read => parent_cap.permissions.read) /\
            (new_permissions.write => parent_cap.permissions.write) /\
            (new_permissions.execute => parent_cap.permissions.execute)
        
        (* 检查请求的资源子集是否在父能力的资源范围内 *)
        resource_valid == 
            IF parent_cap.type = "memory" THEN 
                LET
                    parent_data == parent_cap.resource_data.data
                    subset_data == resource_subset
                IN
                    subset_data.base >= parent_data.base /\ 
                    (subset_data.base + subset_data.size) <= (parent_data.base + parent_data.size)
            ELSE 
                (* 其他资源类型的检查类似 *)
                TRUE
        
        (* 创建新能力 *)
        new_cap_id == cms.next_cap_id
        new_cap == [
            id |-> new_cap_id,
            type |-> parent_cap.type,
            owner_id |-> parent_cap.owner_id,  (* 继承父能力的拥有者 *)
            permissions |-> new_permissions,
            resource_data |-> [
                type |-> parent_cap.resource_data.type,
                data |-> resource_subset
            ]
        ]
        
        new_capabilities == Append(cms.capabilities, new_cap)
        
        new_state == IF parent_valid /\ permissions_valid /\ resource_valid THEN 
            [cms EXCEPT 
                !capabilities = new_capabilities,
                !next_cap_id = cms.next_cap_id + 1
            ]
        ELSE 
            cms
    IN
        new_state

(* 设置服务层能力 *)
SetServiceLayerCapabilities(cms, mem_cap, cpu_cap) == 
    [cms EXCEPT 
        !service_layer_mem_cap = mem_cap,
        !service_layer_cpu_cap = cpu_cap
    ]

(* 获取服务层初始能力 *)
GetServiceLayerCapabilities(cms) == 
    [
        mem_cap |-> cms.service_layer_mem_cap,
        cpu_cap |-> cms.service_layer_cpu_cap
    ]

(* 下一步状态关系 *)
Next(cms, cms') == 
    (* 创建能力操作 *)
    (\E resource_data \in ResourceData : 
        cms' = CreateCapability(cms, resource_data)
    ) \/ 
    
    (* 获取能力操作 *)
    (\E cap_id \in CapabilityId : 
        cms' = AcquireCapability(cms, cap_id)
    ) \/ 
    
    (* 释放能力操作 *)
    (\E cap_id \in CapabilityId : 
        cms' = ReleaseCapability(cms, cap_id)
    ) \/ 
    
    (* 派生能力操作 *)
    (\E parent_cap_id \in CapabilityId, new_permissions \in [read:Bool, write:Bool, execute:Bool], resource_subset : 
        cms' = DeriveCapability(cms, parent_cap_id, new_permissions, resource_subset)
    ) \/ 
    
    (* 设置服务层能力操作 *)
    (\E mem_cap, cpu_cap \in CapabilityId : 
        cms' = SetServiceLayerCapabilities(cms, mem_cap, cpu_cap)
    )

(* 系统行为 *)
Spec == Init /\ [][Next]_<<cms.capabilities, cms.next_cap_id, cms.service_layer_mem_cap, cms.service_layer_cpu_cap>>

(* 不变式：能力ID唯一 *)
UniqueCapabilityIds == \A i, j \in DOMAIN cms.capabilities : 
    i # j => cms.capabilities[i].id # cms.capabilities[j].id

(* 不变式：派生能力的权限不超过父能力 *)
DerivedCapabilityPermissionsLimited == \A dc \in cms.capabilities : 
    (* 这里简化处理，假设所有派生能力都有一个父能力 *)
    (* 实际系统中需要记录能力之间的派生关系 *)
    TRUE  (* 占位符，实际验证需要更复杂的逻辑 *)

(* 不变式：服务层能力有效 *)
ServiceLayerCapabilitiesValid == 
    (cms.service_layer_mem_cap = 0 \equiv cms.service_layer_cpu_cap = 0) /\
    (cms.service_layer_mem_cap # 0 => 
        \E c \in cms.capabilities : c.id = cms.service_layer_mem_cap /\ c.type = "memory"
    ) /\
    (cms.service_layer_cpu_cap # 0 => 
        \E c \in cms.capabilities : c.id = cms.service_layer_cpu_cap /\ c.type = "cpu"
    )

(* 验证条件 *)
THEOREM CapabilitySystemCorrectness == Spec => 
    []UniqueCapabilityIds /\ 
    []DerivedCapabilityPermissionsLimited /\ 
    []ServiceLayerCapabilitiesValid

=============================================================================